module TTAH where 

import Domain
import Model

c1 :: Bool -> Bool
c1 _ = True 

c0 :: Bool -> Bool
c0 _ = False

disj :: Bool -> Bool -> Bool
disj True  = c1
disj False = id

self :: (a -> a -> b) -> a -> b
self f x = f x x 

r :: Entity -> Entity -> Bool
r A A = True 
r A _ = False 
r B B = True 
r B C = True 
r B _ = False 
r C C = True 
r _ _ = False 

inv2     :: (a -> b -> c) -> ((b,a) -> c)
inv2 f p  = f (snd p) (fst p) 

e1         :: (a,b,c) -> a
e1 (x,y,z)  = x
e2         :: (a,b,c) -> b
e2 (x,y,z)  = y
e3         :: (a,b,c) -> c
e3 (x,y,z)  = z

inv3     :: (a -> b -> c -> d) -> ((c,b,a) -> d)
inv3 f t  = f (e3 t) (e2 t) (e1 t) 

g :: Entity -> Entity -> Entity -> Bool
g D x y = r x y 
g E x y = not (r x y)
g _ _ _ = False 

data Var = X Int deriving (Eq,Ord)

instance Show Var where 
  show (X 0) = "x" 
  show (X i) = 'x' : show i

data Form =  Atom String [Var]
           | Eq Var Var
           | Neg Form
           | Impl Form Form
           | Equi Form Form 
           | Conj [Form]
           | Disj [Form] 
           | Forall Var Form 
           | Exists Var Form
     deriving (Eq,Ord)

instance Show Form where 
  show (Atom str []) = str
  show (Atom str ts) = str ++ concat [ show ts ]
  show (Eq t1 t2)   = show t1 ++ "==" ++ show t2
  show (Neg form)   = '~': (show form)
  show (Impl f1 f2) = "(" ++ show f1 ++ "==>" ++ show f2 ++ ")"
  show (Equi f1 f2) = "(" ++ show f1 ++ "<=>" ++ show f2 ++ ")"
  show (Conj []) =  "true" 
  show (Conj fs) =  "conj" ++ concat [ show fs ]
  show (Disj []) =  "false" 
  show (Disj fs) =  "disj" ++ concat [ show fs ]
  show (Forall v f) = "A" ++  show v ++ (' ' : show f)
  show (Exists v f) = "E" ++  show v ++ (' ' : show f)

form1 = Forall (X 0) (Atom "R" [X 0,X 0])
form2 = Forall (X 0) 
         (Forall (X 1) (Impl (Atom "R" [X 0,X 1]) (Atom "R" [X 1,X 0])))

